\begin{tabbing}
st{-}lookup(${\it tab}$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let $K$,$p$,$f$ = ${\it tab}$ in \+
\\[0ex]let $n$ = mu($\lambda$$n$.$p$$<_{2}$$n$ $\vee_{2}$ $K$$\leq_{2}$$n$ $\vee_{2}$ eq\_atom1(1of($f$($n$));$x$)) in 
\\[0ex]if $p$$<_{2}$$n$ $\vee_{2}$ $K$$\leq_{2}$$n$$\rightarrow$ inr($\cdot$) else inl(2of($f$($n$))) fi
\-
\end{tabbing}